/* Hybrid System Abstractor
 *
 * Copyright (c) 2013, Fortiss GmbH - An-Institut TU Muenchen
 *
 * This program is free software: you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation, either version 3 of the License, or
 * (at your option) any later version.
 *
 * This program is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with this program.  If not, see <http://www.gnu.org/licenses/>.
 */
package org.fortiss;

import javax.xml.bind.*;
import java.util.*;
import java.io.*;
import org.fortiss.util.*;
import org.fortiss.automaton.*;
import java.util.ArrayList;

public class HybridSystemAbstractor
{
    public static void main(String[] args) throws Exception
    {
        String ex = "converter";
        // createExample(ex);

        File fHybSys = new File("example/" + ex + "-model.xml");
        JAXBContext ctxHybSys = JAXBContext.newInstance(Automaton.class, Interval.class);
        Unmarshaller umsHybSys = ctxHybSys.createUnmarshaller();
        HybridSystem hs = (HybridSystem) umsHybSys.unmarshal(fHybSys);
        
        File fPredList = new File("example/" + ex + "-predicate.xml");
        JAXBContext ctxPredList = JAXBContext.newInstance(ListWrapper.class, Predicate.class);
        Unmarshaller umsPredList = ctxPredList.createUnmarshaller();
        @SuppressWarnings("unchecked")
        List<List<Predicate>> predList = unwrap(((ListWrapper<ListWrapper<Predicate>>) umsPredList.unmarshal(fPredList)));
        
        File fInitialCondition = new File("example/" + ex + "-initcond.xml");
        JAXBContext ctxPredicate = JAXBContext.newInstance(Predicate.class);
        Unmarshaller umsPredicate = ctxPredicate.createUnmarshaller();
        Predicate initCond = (Predicate) umsPredicate.unmarshal(fInitialCondition);
        
        PredicateAbstractor abstractor = new PredicateAbstractor();
        KripkeStructure b = abstractor.abstractWithPredicate(hs, predList, initCond, 2);
        
        File fKS = new File("example/" + ex + "-abstraction.xml");
        JAXBContext ctxKS = JAXBContext.newInstance(Automaton.class);
        Marshaller msKS = ctxKS.createMarshaller();
        msKS.setProperty(Marshaller.JAXB_FORMATTED_OUTPUT, Boolean.TRUE);
        msKS.marshal(b, fKS);
    }
    
    private static ListWrapper<ListWrapper<Predicate>> wrap(List<List<Predicate>> llp)
    {
        ListWrapper<ListWrapper<Predicate>> ret = new ListWrapper<ListWrapper<Predicate>>(llp.size());
        for (int i=0; i<llp.size(); i++)
            ret.add(new ListWrapper<Predicate>(llp.get(i)));
        return ret;
    }
    
    private static List<List<Predicate>> unwrap(ListWrapper<ListWrapper<Predicate>> llp)
    {
        List<List<Predicate>> ret = new ArrayList<List<Predicate>>(llp.size());
        for (int i=0; i<llp.size(); i++)
            ret.add(llp.get(i).unwrap());
        return ret;
    }
    
    private static void createExample(String name) throws Exception
    {
        File fHybSys = new File("example/" + name + "-model.xml");
        JAXBContext ctxHybSys = JAXBContext.newInstance(Automaton.class, Interval.class);
        HybridSystem hs0 = createBoostConverter();
        Marshaller msHybSys = ctxHybSys.createMarshaller();
        msHybSys.setProperty(Marshaller.JAXB_FORMATTED_OUTPUT, Boolean.TRUE);
        msHybSys.marshal(hs0, fHybSys);
        
        File fPredList = new File("example/" + name + "-predicate.xml");
        JAXBContext ctxPredList = JAXBContext.newInstance(ListWrapper.class, Predicate.class);
        List<Predicate> g1 = Arrays.asList(new Predicate[]{
            new Predicate(new double[][]{{1, 0, 0.2}}, null),
            new Predicate(new double[][]{{1, 0, 0.9}}, new double[][]{{-1, 0, -0.2}}),
            new Predicate(new double[][]{{1, 0, 1.6}}, new double[][]{{-1, 0, -0.9}}),
            new Predicate(new double[][]{{1, 0, 2.3}}, new double[][]{{-1, 0, -1.6}}),
            new Predicate(null, new double[][]{{-1, 0, -2.3}}),
            });
        List<Predicate> g0 = Arrays.asList(new Predicate[]{
            new Predicate(new double[][]{{0, 1, 3}}, null),
            new Predicate(new double[][]{{0, 1, 3.2}}, new double[][]{{0, -1, -3}}),
            new Predicate(new double[][]{{0, 1, 3.4}}, new double[][]{{0, -1, -3.2}}),
            new Predicate(new double[][]{{0, 1, 3.6}}, new double[][]{{0, -1, -3.4}}),
            new Predicate(null, new double[][]{{0, -1, -3.6}}),
            });
        List<List<Predicate>> predList0 = new ArrayList<List<Predicate>>(2);
        predList0.add(g0);
        predList0.add(g1);
        Marshaller msPredList = ctxPredList.createMarshaller();
        msPredList.setProperty(Marshaller.JAXB_FORMATTED_OUTPUT, Boolean.TRUE);
        msPredList.marshal(wrap(predList0), fPredList);
        
        File fInitialCondition = new File("example/" + name + "-initcond.xml");
        JAXBContext ctxPredicate = JAXBContext.newInstance(Predicate.class);
        Marshaller msPredicate = ctxPredicate.createMarshaller();
        msPredicate.setProperty(Marshaller.JAXB_FORMATTED_OUTPUT, Boolean.TRUE);
        Predicate predInit = new Predicate(
            new double[][]{
                {0, 1, 3.4},
                {1, 0, 1.6}},
            new double[][]{
                {0, -1, -3.2},
                {-1, 0, -0.9}});
        msPredicate.marshal(predInit, fInitialCondition);
    }
    
    private static HybridSystem createRollerCoaster()
    {
        HybridSystem a = new HybridSystem();
        a.setName("Car");
        a.setStateVariable(Arrays.asList(new String[]{"x", "v"}));
        
        IntervalMatrix A = new IntervalMatrix(new double[][]{
            {0, 1},
            {0, 0}});
        
        Predicate p = new Predicate(null,
            new double[][]{
            {-1.0, 0, 0},
            {0, -1.0, 0}});
        
        HybridNode du = new HybridNode();
        du.init(0, "slow down uphill (-1)", true, p, null);
        du.setFlow(
            A.addCoefficient(
            new IntervalMatrix(new double[][]{
                {0},
                {-1}
            })));
        HybridNode uu = new HybridNode();
        uu.init(1, "speed up uphill (+0.5)", false, p, null);
        uu.setFlow(
            A.addCoefficient(
            new IntervalMatrix(new double[][]{
                {0},
                {0.5}
            })));
        HybridNode dd = new HybridNode();
        dd.init(2, "slow down downhill (-0.5)", false, p, null);
        dd.setFlow(
            A.addCoefficient(
            new IntervalMatrix(new double[][]{
                {0},
                {-0.5}
            })));
        HybridNode ud = new HybridNode();
        ud.init(3, "speed up downhill (+1)", false, p, null);
        ud.setFlow(
            A.addCoefficient(
            new IntervalMatrix(new double[][]{
                {0},
                {1}
            })));
        
        Predicate peq = new Predicate(null, new double[][]{
            {1, 0, 50},
            {-1, 0, -50}});
        IntervalMatrix u = new IntervalMatrix(new double[][]{
            {0, 0, 0},
            {0, 1, 0}});
        
        AutonomousUpdateEdge du2dd = new AutonomousUpdateEdge();
        du2dd.init(peq, dd.getID(), u);
        AutonomousUpdateEdge uu2ud = new AutonomousUpdateEdge();
        uu2ud.init(peq, ud.getID(), u);
        AutonomousUpdateEdge ud2uu = new AutonomousUpdateEdge();
        ud2uu.init(peq, uu.getID(), u);
        AutonomousUpdateEdge dd2du = new AutonomousUpdateEdge();
        dd2du.init(peq, du.getID(), u);
        
        IntervalMatrix unchanged =
                new IntervalMatrix(new double[][]{
                    {1, 0, 0},
                    {0, 1, 0}
                });
        
        ControlledUpdateEdge du2uu = new ControlledUpdateEdge();
        du2uu.init(1, uu.getID(), unchanged);
        ControlledUpdateEdge uu2du = new ControlledUpdateEdge();
        uu2du.init(0, du.getID(), unchanged);
        ControlledUpdateEdge dd2ud = new ControlledUpdateEdge();
        dd2ud.init(1, ud.getID(), unchanged);
        ControlledUpdateEdge ud2dd = new ControlledUpdateEdge();
        ud2dd.init(0, dd.getID(), unchanged);
        
        du.addEdge(du2dd);
        du.addEdge(du2uu);
        uu.addEdge(uu2ud);
        uu.addEdge(uu2du);
        ud.addEdge(ud2uu);
        ud.addEdge(ud2dd);
        dd.addEdge(dd2du);
        dd.addEdge(dd2ud);
        
        a.addNode(du);
        a.addNode(du);
        a.addNode(uu);
        a.addNode(dd);
        a.addNode(ud);
        
        return a;
    }

    private static HybridSystem createBoostConverter()
    {
        double v = 1.5, L = 150, C = 110, R = 6;
        HybridSystem a = new HybridSystem();
        a.setName("Boost Converter");
        a.setStateVariable(Arrays.asList(new String[]{"i", "v"}));
        
        
        Predicate p = new Predicate(
            new double[][]{
            {1.0, 0, 3.9},
            {0, 1.0, 4.9}},
            new double[][]{
            {-1.0, 0, 1.9},
            {0, -1.0, -1.1}});

        HybridNode q1 = new HybridNode();
        q1.init(0, "SW1 on, SW2 off", true, p,
            new IntervalMatrix(new double[][]{
            {0, 0,     v/L},
            {0, -1/R/C, 0}}));
        
        HybridNode q2 = new HybridNode();
        q2.init(1, "SW1 off, SW2 on", false, p, 
            new IntervalMatrix(new double[][]{
            {0,     -1/L, v/L},
            {1/C, -1/R/C, 0}}));
        
        IntervalMatrix unchanged =
                new IntervalMatrix(new double[][]{
                    {1, 0, 0},
                    {0, 1, 0}
                });
        
        ControlledUpdateEdge t12 = new ControlledUpdateEdge();
        t12.init(1, q2.getID(), unchanged);
        ControlledUpdateEdge t21 = new ControlledUpdateEdge();
        t21.init(0, q1.getID(), unchanged);
        
        q1.addEdge(t12);
        q2.addEdge(t21);
        
        a.addNode(q1);
        a.addNode(q2);
        
        return a;
    }
}